Досрочный экзамен по математической логике 25 декабря 2004 года время на выполнение работы: 2,5 часа Условия задач: NB: в Oper'е замечена проблема с шрифтом Symbol Текст – это конечный список слов. Слово – это конечный список литер. Написать программу, ищущую самое короткое слово Х из самых часто встречающихся в тексте L слов. Запрос ? G(L, X) Выразить на языке логики предикатов следующее утверждение в виде замкнутой формулы: "Если почти все элементы последовательности действительных чисел y равны между собой, то и предел последовательности равен этому же числу". доступные константы: 0 – константа 0 доступные функциональные символы |x| - абсолютное значение х (-х) - смена знака х x+y, x-y, x*y, x/y - арифметические операции доступные предикаты: R(x) - вещественное число N(x) - натуральное число S(y) - y - последовательность действительных чисел E(x,n,y) - x - элемент y с номером n L(p,y) - p - предел последовательности y x < y, x > y, x = y – сравнение и равенство С помощью метода семантических таблиц исследовать общезначимость данной формулы: ($y ¬P(x) > $x R(x)) > ("x $y (¬P(x) > R(y))) С помощью метода резолюций исследовать общезначимость данной формулы: ($y ¬P(x) > $x R(x)) > ("x $y (¬P(x) > R(y))) Изобразить дерево SLD-резолютивных вычислений и дать все вычислимые ответы для следующей программы: ? P(x), R(x) P(b) < ; P(f(b)) < R(b), !; P(c) < ; R(f(x)) < P(x); R(x) < P(x); Дать определение противоречивого множества замкнутых формул Дать определение SLD-резолютивного опровержения Дать определение эрбрановской интепретации формулы j Операционная семантика оператора not в логическом программировании Таблица aГ; Dn состоит из замкнутых формул и не имеет успешных вычислений. Какие утверждения верны всегда и почему? Г имеет хотя бы одну модель D имеет хотя бы одну модель ни одна из ?ID не является общезначимой ни одно из утверждений a-c не верно Пусть S – множество дизъюнктов. Пусть S' – множество всех резольвент, получаемых из S. Какие из следующих утверждений несправедливы и почему? если S – непротиворечивое множество, то S' – непротиворечивое множество если S – противоречивое множество, то S' – противоречивое множество если S' – непротиворечивое множество, то S – непротиворечивое множество если S’ – противоречивое множество, то S – противоречивое множество среди a-d есть неверное утверждение, но его номер зависит от S Пусть I – эрбрановская интерпретация логической программы П такая, что TП(I) C I = TП(I) ? I (TП - оператор непосредственного следования). Какие из следующих утверждений верны независимо от I и П и почему? SuccП I I SuccП I I SuccП = I SuccП E I SuccП E I ни одно из a-e неверно в общем случае Ответы: программа, работающая на PDC-PROLOG пример оформления этой задачи domains word = char* text = word* predicates G(text, word) is_most_often(text, word) exists_more_often(text, word) occur(text, word, integer) elem(text, word) length(word, integer) exists_more_short(text, word) clauses G(L, X) :- elem(L, X), is_most_often(L, X), not(exists_more_short(L, X)), !. is_most_often(L, X) :- not(exists_more_often(L, X)). exists_more_often(L, X) :- elem(L, Y), not(Y = X), occur(L, X, K), occur(L, Y, K1), K1 > K, !. elem([X|_], X). elem([_|L], X) :- elem(L, X). occur([], _, 0). occur([X|L], X, K1) :- !, occur(L, X, K), K1 = K+1. occur([_|L], X, K1) :- occur(L, X, K1). exists_more_short(L, X) :- elem(L, Y), is_most_often(L, Y), length(X, LX), length(Y, LY), LX > LY. length([], 0). length([_|L], K1) :- length(L, K), K1 = K+1. G(L, X) < elem(L, x), is_most_often(L, x), not(exists_more_short(L, x)), !; is_most_often(L, x) < not(exists_more_often(L, x)); exists_more_often(L, x) < elem(L, y), not(y = x), occur(L, x, k), occur(L, y, k1), k1 > k, !; occur(nil, x, 0) < ; occur(x.L, x, k1) < !, occur(L, x, k), k1 is k+1; occur(y.L, x, k1) < occur(L, x, k1); exists_more_short(L, x) < elem(L, y), is_most_often(L, y), length(x, Lx), length(y, Ly), Lx > Ly; length(nil, 0) < ; length(y.L, k1) < length(L, k), k1 is k+1; "y ( S(y) > "l ( R(l) > ( ( $n ( N(n) & "m ( N(m) & m > n > $x ( R(x) & E(x, m, y) & l = x ) ) ) > $lim ( R(lim) & L(lim, y) & l = lim ) ) ) ) общезначима общезначима {x / b}, {x / f(b)} - 9. - см. лекции ответ: a, c верно, т.к. иначе бы по определению выполнимости таблицы таблица имела успешный вывод неверно. контпример: < | P(a) & ¬P(a) > верно, т.к. иначе бы таблица по теореме Геделя имела успешный вывод неверно, т.к. верно а ответ: b, c, e всегда верно по лемме о резолюции к теореме о корректности метода резолюций несправедливо: контпример = { P(x) \/ P(y), ¬P(x) \/ ¬P(y) } несправедливо, см. контпример пункта b всегда верно по лемме о резолюции к теореме о корректности метода резолюций несправедливо: контрпример = { P, ¬P } ответ: a, b верно, т.к. I E TП(I) => I ETП(I) => TП(I)E TП(TП(I)) = TП2(I) => I E TП(I) E TП2(I) E TП3(I) E ... . Есть 2 варианта завершения: цепочка сойдется. Тогда мы придем к lfpП = SuccП, поскольку наименьшая неподвижная точка единственна. Но тогда смотрим начало и конец цепочки: I E SuccП, что доказывает начальное утверждение. цепочка будет уменьшаться до ?. Но что с ней произойдет потом? Пусть мы получили пустое множество на шаге k, т.е. TПk(I) = ?, но TПk(I) E TПk+1(I), т.е. ? E TП(?), но для любого ОНС верно и то, что ? I TП(?) (пустое множество вложено в любое множество). Т.е. ? = TП(?). Т.е. если цепочка дошла до пустого множества, то и наименьшая неподвижная точка равна пустому множеству (она же единственна). Но тогда I E TП(I) E ? = lfpП = SuccП, т.е. I E SuccП, что также доказывает начальное утверждение верно, т.к. верно b неверно, т.к. при этом I = SuccП = lfpП => I = TП(I) по определению неподвижной точки. Но I E TП(I) по условию. Противоречие. неверно, т.к. при этом I I SuccП = lfpП => SuccП не является наименьшей неподвижной точкой (есть вложенная интерпретация). Противоречие. неверно, т.к. неверны c и d неверно, т.к. верно b NB: мне больше всего понравилась последняя задача (на самом экзамене я до такого доказательства пункта b даже и не догадался), тем что она красивая (не надо ломать голову над контрпримерами, а надо просто хорошо знать все формулировки теорем и определения). Прекрасно, что для решения 10-12 задач действительно достаточно их знать и здраво и логично рассуждать (я на экзамене забыл про единственность lfp, поэтому, наверное, и не придумал доказательства пункта b 12й задачи, ведь оно главным образом использует эту единственность). Иногда, конечно, приходится придумывать контрпримеры, но бывает полезно взять контпример из лекций: контрпример к пункту b 11й задачи прямо был упомянут Захаровым ("склейка важна"). Мы писали экзамен 2,5 часа - и этого как раз вполне хватает для того, чтобы сделать 12 задач (как 100 минут как раз хватает для выполнения всех 10 заданий Мальковского). Писали мы без перерыва и не сдавали отдельно задачу на пролог (сдали всё в самом конце).